Formal verification techniques such as symbolic model checking (SMC)—that use binary decision diagrams (BDDs)—offer the potential of exhaustive coverage and the ability to detect subtle bugs unlike traditional techniques such as simulation. These techniques that use BDDs however, are known to suffer from a state explosion problem and consequently fail for circuits having a large number of flip-flops/state variables.
Boolean Satisfiability (SAT) solvers have exhibited numerous attributes that make them attractive complements to BDDs. In particular, their performance is less sensitive to size and they typically do not suffer from the state explosion problem noted before. As a result, the development of routines that perform bounded model checking (BMC) utilizing SAT methodologies has been the subject of much research.
Unlike symbolic model checking, BMC focuses on finding bugs of bounded length, and successively increases the boundaries in search of longer traces. Given a design and a correctness property, BMC generates a Boolean formula, such that the formula is true if and only if there exists a witness/counterexample of length k. This Boolean formula is then checked by a backend SAT solver. Advantageously, and due in part to recent advances made to SAT solvers, SAT-based BMC can handle much larger designs and analyze them faster then ever before.
By way of example, Burch and Dill, in a paper entitled “Automatic Verification of Pipelined Microprocessor Control” which appeared in Proceedings of the sixth International Conference on Computer-Aided Verification, volume 818, D. L. Dill, Ed.: Springer-Verlag, 1994, pp. 68-80, introduced symbolic representation of memory arrays in their logic of equality with un-interpreted functions. Their abstract interpretation of memory uses interpreted read and write operations. These interpreted functions are used to represent the memory symbolically by creating nested if-then-else (ITE) structure to record the history of writes to the memory.
In an effort to model an entire circuit with control and data memory, Velev et al., in an article entitled “Efficient Modeling of Memory Arrays in Symbolic Simulation”, that appeared in Computer Aided Verification, O. Grumberg, Ed., pp. 399-399 in 1987, introduced a behavioral model that allows the number of symbolic variables used to be proportional to the number of memory accesses rather than to the size of the memory. This model replaces the memory and it interacts with the rest of the circuit through a software interface. Similar to that shown by Burch and Dill, the Velev et al. read and write operations are defined in such a way that the forwarding property of the memory semantics (i.e., data read from a memory location is the same as the recent data written at the same location) is satisfied. Unfortunately however, BDDs used to represent the Boolean expressions tend to “blowup” for processors with branch or load/store instruction(s) and good BDD ordering is not possible due to dependencies of address on the data and vice-versa.
In an article entitled “Processor Verification Using Efficient Reductions for the Logic of Uninterpreted Functions to Propositional Logic”, that appeared in ACM Transactions on Computational Logic (TOCL) on pp. 93-134, Vol., 2, No. 1, in January 2001, R. E. Bryant, S. German, and M. N. Velev discovered that for processors in which writes are not reordered relative to each other or to reads, it is sufficient to represent data memory as a generic state machine, changing state in some arbitrary way for each write operation, and returning some arbitrary value dependent on the state and address for each read operation. Such an abstraction is sound, but it does not capture all the properties of a memory.
Subsequently, Velev (see, M. N. Velev, “Automatic Abstraction of Memories in the Formal Verification of Superscalar Microprocessors, ” Proceeding of Tools and Algorithms for the Construction and Analysis of Systems, 2001, pp. 252-267), automated the process of abstraction of data memory by applying a system of conservative transformation rules and generating hybrid memory model(s) where forwarding semantics of memory is satisfied only for some levels of forwarding.
More recently, Bryant et al., in an articled entitled “Modeling and Verifying Systems using a Logic of Counter Arithmetic with Lambda Expressions and Uninterpreted Functions”, that appeared in Computer-Aided Verification in 2002, proposed logic to model infinite-state systems and unbounded memory in a system named UCLID. According to this article, memory is modeled as a function expression whose body can change with time step(s). Similar to that shown by Burch and Dill, the memory is represented symbolically by creating nested if-then-else (ITE) structure to record the history of writes to the memory. In this restricted Counter arithmetic with Lambda Expressions and Uninterpreted Functions (CLU) logic, one can use BMC to verify safety properties.
Despite these advances however, SAT-based BMC is still unable to handle designs involving large embedded memories and therefore, more thorough, efficient, and expedient approaches are required. Such enhancements to SAT-based BMC would represent a significant advance in the art and is therefore the object of the present invention.
Additionally, and according to a Semiconductor Industry Association roadmap prediction, embedded memories will comprise more than 70% of the System on a Chip (SoC) devices by 2005. These embedded memories on SoC support diverse code and data requirements arising from an ever increasing demand for data throughput in applications ranging from cellular phones, smart cards and digital cameras.
Efforts to verify on-chip memory arrays using Symbolic Trajectory Evaluation are fraught with difficulty as embedded memories dramatically increase both design and verification complexity due to an exponential increase in the state space with each additional memory bit. In particular, this state explosion adversely affects the practical application of formal verification techniques like model checking for functional verification of such large embedded memory systems.
To tame the verification complexity, several memory abstraction techniques, i.e., removing the memories partially or completely from the designs are often used in the industry. However, such techniques often produce spurious outcomes, adversely affecting overall verification efforts. In many refinement-based techniques, starting from a small abstract model of the concrete design, spurious counter-examples on the abstract model are used to refine the model iteratively. In practice, several iterations are needed before a property can be proved correct or a real counter-example can be found. Note that after every iterative refinement step, the model size increases, making it increasingly difficult to verify.
In contrast, abstraction-based approaches use proof-based abstraction (PBA) techniques on a concrete design. As shown by the inventors in a paper entitled “Iterative Abstraction using SAT-based BMC with Proof Analysis”, which appeared in the Proceedings of International Conference on Computer Aided Design in 2003, iterative abstraction can be used to apply such techniques on progressively more abstract models, thereby leading to significant reduction in model size. However, since these approaches use the concrete model to start with, it may not be feasible to apply them on designs with large memories. In general, both these refinement and abstraction based approaches are not geared towards exploiting the memory semantics.